package ch.epfl.lara.matcheck.verify.axioms;

import ch.epfl.lara.matcheck.ast._
import ch.epfl.lara.matcheck.util.FreshName

trait ObjectAxioms extends IAxiom
                   with    PropositionalFormulaMaker
{ 
  import ifc._
  import Constants.{UNAPPLY,DOM_PREPEND,EXTR_PREPEND,SEP}
  
  private var _extractors_results: Axiom = _
  private var _extractors_domains: Axiom = _
  
  /**
   * <p>
   *    From the declared objects, filter the ones that contains the unapply method:
   *        this object are extractors. Then derive all typing relation between an extractor
   *        and the respective class to which it applies.
   * </p>
   */
  protected def objectsAxioms(objects: List[ObjectDef]) {
    var subtype: Formula = Tru
    var result_unapply: Formula = Tru
    
    for(ObjectDef(name,invariant,methods) <- objects 
          if methods.exists(m => m.getName == UNAPPLY)) yield {
      val MethodDef(_,params,retTpe,_,_) = methods.find(_.getName == UNAPPLY).get
      assert(params.size == 1) // extractors takes always one parameter 
      val ParamDef(argName,argType) = params.head
      val domaine: String = DOM_PREPEND+name.getName
        
      // Extr_Object <: Type_argument
      subtype = And(subtype,SubsetEq(Set(domaine),Set(argType.toString)))
      
      // ALL fresh_v \in argName.getType --> Extr_object_i(fresh_v) \in RetType_i
      val extractor_name: String = EXTR_PREPEND+name.getName
      val fresh = FreshName.fresh(argName.getName)
      val returnSet: Formula = (retTpe: @unchecked) match {
        case IntType | BoolType => Function(extractor_name+SEP+"1",Element(fresh) :: Nil) //XXX: Should I put type informations
        case ClassType(_) => In( Function(extractor_name+SEP+"1",Element(fresh) :: Nil),
                                               Set(retTpe.toString))
        case OptionType(tpe :: Nil) => In( Function(extractor_name+SEP+"1",Element(fresh) :: Nil),
                                           Set(tpe.toString))                                                    
        case OptionType(xs) => 
          conjunction(xs.zipWithIndex.map(pair => 
                                 In( Function(extractor_name+SEP+(pair._2+1),Element(fresh) :: Nil),
                                     Set(pair._1.toString)))
                      )
      }
        
      val right_implication = Forall(fresh,Imply(In(Element(fresh),Set(argType.toString)),returnSet))
      val left_implication = Forall(fresh,Imply(returnSet,In(Element(fresh),Set(argType.toString))))
      result_unapply = And(result_unapply,And(right_implication,left_implication))
    }
    
    _extractors_domains = subtype
    _extractors_results = result_unapply
   }
	
  def extractors_results : Axiom = _extractors_results
  def extractors_domains: Axiom = _extractors_domains 
}
